trait solver: Capture binder region constraints while relating - #157984

r? @mejrs

rustbot has assigned @mejrs.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

r? @lcnr

r? BoxyUwU

BoxyUwU is currently at their maximum review capacity.
They may take a while to respond.

@BoxyUwU fwiw, i think the ci failure is still compatible with your suggestion. the direct registration path lgtm to me, but the current version is probably registering from too many relation contexts.

the bad bit seems to be solverrelating::regions(): under -zassumptions-on-binders it always pushes regionoutlives into the solver constraint storage. some of those relation calls happen under enter_forall_with_empty_assumptions, so later placeholder handling has no assumptions to discharge the constraint and we hit the max_universe(...) < u assert.

imo the fix is not to go back to manually bubbling a list everywhere. i'd rather keep direct registration, but only in contexts where the solver owns the binder assumptions, or keep the constraints local while relating a binder and pull them out before registering. idk which shape is cleaner yet, but unconditional registration in regions() seems too wide.

follow-up after pushing 0d93b4c:

i tried to keep the direct-registration shape, but idk, it still looked too broad in practice. buffering constraints around binder relation did not clear the reported failures for me.

imo the safer fix is to keep the region constraints local while relating, then register the collected next-gen constraint only from the solver-owned relation entrypoints. ltm this still follows the direction boxy was pointing at, without letting solverrelating::regions() register constraints from the empty-assumption binder probes.

i checked the same failure cases locally:

• x.py check compiler/rustc_type_ir compiler/rustc_next_trait_solver
• x.py test tests/ui/assumptions_on_binders/alias_outlives.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-1.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-2.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-3.rs tests/ui/assumptions_on_binders/principal-upcast-region-eq-issue-157859.rs tests/ui/assumptions_on_binders/trait-upcast-projection-region-eq.rs
• x.py test tidy

some of those relation calls happen under enter_forall_with_empty_assumptions, so later placeholder handling has no assumptions to discharge the constraint and we hit the max_universe(...) < u assert.

in theory that shouldn't cause us to hit an assert. if we have empty assumptions then we'll rewrite the constraints to false and (eventually) get an error 🤔 if we were doing this in a enter_forall_without_assumptions it would make sense to me we get ICEs. though I wouldn't expect it to be due to the max_universe(..) < n assertion 🤔 I would expect it to be due to missing entries in the assumptions list in the InferCtxt.

i would like to fully understand what's going on with the ICEs when always registering the next gen region constraints :3 can you look more into what's going on there, if you could push the code that causes those ICEs to happen so I can see the CI failure too that would be useful :3

i looked into the unconditional direct-registration version locally.

imo it confirms the failure mode from my earlier guess: the new repro tests pass, but the broader assumptions-on-binders set fails.

specifically:

• alias_outlives.rs hits the max_universe(infcx, constraint.clone()) < u assertion
• the type_relation_binders_inside_solver-* tests either ice or reject code that should pass

so idk, direct registration from solverrelating::regions() still feels too broad to me. lgtm in principle, but only if we can keep it out of binder probes with empty assumptions. ltm the current local-collection shape is the safer boundary for now: collect while relating, then register from the solver-owned relation entrypoints.

i can push the failing experiment to a separate branch if seeing ci on that exact shape would help, but i'd rather not force-push it over this pr branch since the current version is passing.

checked with:

• x.py check compiler/rustc_type_ir compiler/rustc_next_trait_solver
• x.py test tests/ui/assumptions_on_binders/alias_outlives.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-1.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-2.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-3.rs tests/ui/assumptions_on_binders/principal-upcast-region-eq-issue-157859.rs tests/ui/assumptions_on_binders/trait-upcast-projection-region-eq.rs
• x.py test tidy

like I said, I don't understand why it's hitting that assertion 😅 can you explain why that assertion is getting hit. i can't properly evaluate this alternate approach without understanding why the other one doesn't work

yeah, my bad! i think i explained the empty-assumptions bit too confidently there.

i pushed the direct registration version again so ci can show the actual failure: 31be28b

idk yet why it ends up at the max_universe assert instead of just rewriting to false, so ltm the useful next step is to let ci capture the full logs on this exact shape.

@rustbot author

gonna do that while you figure out what's going on there, if you're having trouble we can chat about it over zulip and try figure it out together

This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed.

Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers.

Ok I've thought about this for a while and I think I know how I'd like to proceed.

To start with I really don't feel confident that I understand the reason why we need this normalization step for turning region vars into placeholders they're known to be equal to. I also think that getting to the point where I am confident I understand it is going to take a while (and already we've spent a bunch of time on this).

But, the core thing this PR is doing is also clearly correct, we definitely want to actually register region constraints when we do type relations 😅

I think what I'd like to do is (unordered list):

• Land the OR thing separately once abby: always store nextgen region constraints in canonical form #161306 has landed
• In a separate PR fix our handling of '!a: '!a constraints (we dont handle 'a: 'a eagerly in some cases (?) project-assumptions-on-binders#19). I think this should be a fairly simple fix (it ought to just be changing a few lines of code to pull_region_outlives_constraints_out_of_universe). That way this PR doesn't need to work around that being broken
• Remove all the unrelated changes from this PR and disable the test that fails without normalization of region variables. implied_higher_ranked_alias_outlives_assumption is kind of a horrible test anyway lmao. Then we can land this without any funny stuff going on and we're closer to stuff being how we want it to be in the long run
• Once we have a better testing DSL for assumptions on binders (support predicates as things to be proven in the testing DSL project-assumptions-on-binders#32) it should be possible to rewrite the failing test into our DSL which should make it lot easier to debug/to be confident in what's going on here and then we can properly evaluate adding this kind of normalization step in its own PR

This of course is all assuming that the breakage here is just that one implied_higher_ranked_alias_outlives_assumption test 🤔

I'm also realising that even if the normalization step is necessary (which I can imagine being the case fwiw), I wouldn't want to land it as part of this PR 🤔 So I think the above steps are probably the right way to go about this regardless so that we get things happening in incremental steps and you can finally get this PR merged 😅

@rustbot author